/*

Mikhail Breslav and Chris Kwan
{breslav, ckwan}@cs.bu.edu
http://cs-people.bu.edu/ckwan/cs511/

CS 511 Spring 2011 Project
Client-side Parsing and Verification

Parser for Propositional Logic

Last update: 04/24/2011

*/


/*
 Initialize text areas and class variables
*/
var message = "Enter an expression, then press Shift-Enter to evaluate it.";        
var instructions = $("instructionsBox");
instructions.value = message;

var outputBox = $("outputBox");
var debugBox = $("debugBox");
var errorBox = $("errorBox");
var tableBox = $("tableBox");
var truthTableBox = $("truthTableBox");
var counterExamplesBox = $("counterExamplesBox");
$("inputBox").focus();

var expressionString = ""; //the expression string being parsed, most methods reference this

var formulaStr = "";
var formulaStrCopy = "";
var formulaTable = new hash_atoms();
var truthTable;

var truthTableNotInitVal = -1;
var startingTruthValue = true;
var numWordsInTable = 0;

var notSym = "not";
var andSym = "and";
var orSym = "or";
var impliesSym = "implies";
var groupLeftSym = "(";
var groupRightSym = ")";
var wordLeftSym = "[";
var wordRightSym = "]";



/*
 Shortcut to get a document element by id.
*/
function $(id)
{
    return document.getElementById(id);
}

/*
 Clear out the values in the output and debug text boxes.
*/
function clearBoxes()
{
    outputBox.value = "";
    debugBox.value = "";
    errorBox.value = "";
    
    tableBox.value = "";
    truthTableBox.value = "";
    formulaTable.clear(); //table of words
    numWordsInTable = 0;
    
    counterExamplesBox.value = "";
}


/*
 Call update method if user presses Shift+Enter.
*/
function keypress(key)
{
    var code = key.charCode;
    if( code == 0 || code == undefined)
        code = key.keyCode;
        
    if(code == 13 && key.shiftKey)
        update();
}    


/*
 Pass the expression from the input box to the parser.
*/
function update()
{
    var input = $("inputBox").value;
    
    //counterExamplesBox.value = "hi";
    
    //alert("pause");
    
    clearBoxes();
    
    //main(input);
    
    //test();
    
    formulaStr = input;
    formulaStrCopy = formulaStr; //keep backup of formula since it will be modified by parser

    cleanupBeforeAssignment();
    
    outputBox.value = expressionValue(0, truthTableNotInitVal);
    
    cleanupAfterAssignment();
        
    //outputBox.value = termValue();
    //outputBox.value = factorValue();    
    //outputBox.value = wordValue();

    //do truth table test
    printTruthTable(formulaTable);
   
    alert("about to reprint truth table");
   
    debugPrintTruthTable();
   
    //counterExamplesBox.value = "";
   
    var isTaut = isFormulaTautology();
   
    alert("isTaut: " + isTaut);
   
   	//testArrays(formulaTable); //testArrays() call.
    alert("done!");
}
function cleanupBeforeAssignment()
{
    //clear debug box (parse tree)
    debugBox.value = "";
    
    
    //outputBox.value = "";
    
    //counterExamplesBox.value = "";
}

function cleanupAfterAssignment()
{
    //restore formulaStr
    formulaStr = formulaStrCopy;
}

function testArrays(table)
{
	var numWords = table.length;
	var numAssignments = Math.pow(2,numWords);
	
	var tt = new Array(numAssignments);
	for(i=0; i<numAssignments; i++)
	{
		tt[i] = new Array(numWords);
	}
	
	
	//assign values to our TT
	
	for(i=0; i<numAssignments; i++)
	{
		for(j=0; j<numWords; j++)
		{
				tt[i][j] = 0;
				truthTableBox.value += tt[i][j] + " ";
		}
		
		truthTableBox.value += "\n";
	}
	
}

function debugPrintTruthTable()
{
    truthTableBox.value = "";
    
	//var numWords = truthTable.length;
	var numWords = formulaTable.length;
    var numAssignments = Math.pow(2,numWords);
    
    for(i=0; i<numAssignments; i++)
	{
        truthTableBox.value += i + ": ";
        
		for(j=0; j<numWords; j++)
		{
			truthTableBox.value += truthTable[i][j] + " ";
		}
		
		truthTableBox.value += "\n";
	}

}

function isFormulaTautology()
{
    //assuming truth table already generated
    
    var isTaut = true;
    
    //alert("truthTable.length: " + truthTable.length);
    
    var numAssn = truthTable.length;
    
    //var numAssn = 2;
  
    //TODO remove later
    outputBox.value = "";
  
    var value;
    //evaluate every assignment (row)
    for(i=0; i<numAssn; i++)
    {
        cleanupBeforeAssignment();
        
        value = expressionValue(0, i);
        
        cleanupAfterAssignment();
        
        if(value == false)
        {
            //alert("add a counter example!");
        
            //add to counterexamples
            
            
            counterExamplesBox.value += "row number: " + i + "\n";
            
            
            
            
            //counterExamplesBox.value = "test";
            
            //outputBox.value += "row number: " + i + "\n";
            
            //alert("after add a counter example!");
            
            isTaut = false;
            //break; //keep going to list all counterexamples
        }
        //if true keep going
        
        outputBox.value += value + "\n";
        
        //alert("value in isTaut: " + value);
    }//end for  
    
    if(isTaut)
    {
        return true;
    }
    else
    {
        return false;
    }
    
    //debugPrintTruthTable();
    
}

/*
 Generate a truth table given a table of words.
*/
function printTruthTable(table)
{
    var numWords = table.length;
	var numAssignments = Math.pow(2,numWords);

	truthTable = new Array(numAssignments);
    
    //initialize 2D Array
    //each row is an assignment
    //and each column is a word
    for(i=0; i<numAssignments; i++)
	{
        truthTable[i] = new Array(numWords);
	}

    //add a title row with word names to the printout
    var titles = "";
    for(var word in table.items)
    {
        titles += word + "\t|";
    }
    truthTableBox.value += titles + "\n";
    
    //print a slight underline
    var underLine = "";
    for(var word in table.items)
    {
        underLine += "__" + "\t|";
    }
    truthTableBox.value += underLine + "\n";

    
    //printTruthTableHelper(0,"",numWords,0);
    //reset current assignment Number
    curAssnNum = 0;
    //printTruthTableHelper(0,"",numWords);
    
    //var tempArray = new Array(numWords);
    //printTruthTableHelper(0,"",numWords, tempArray );
    
    printTruthTableHelper(0,"",numWords);
}
var itemValsArray = new Array();
var curAssnNum = 0; //global
/*
 Helper method for printing out all truth values in truth table.
*/
//function printTruthTableHelper(curItemIndex, strSoFar, numItems, curAssnNum)
function printTruthTableHelper(curItemIndex, strSoFar, numItems)
//function printTruthTableHelper(curItemIndex, strSoFar, numItems, itemValsArray)
{
    var numTruthVals = 2; //0 and 1
    
    //at the last column of the table, print out the row
    if(curItemIndex == numItems-1)
    {
        for(var k=0; k<numTruthVals; k++)
        {
            var truthVal;
            if(k==0)
            {
                truthVal = false;
            }
            else if(k==1)
            {
                truthVal = true;
            }
            truthTable[curAssnNum][curItemIndex] = truthVal;
            
            //alert("in if storing: " + curAssnNum + ", " + curItemIndex + ": " + truthVal);
            
            //display the current assignment
            var truthStr;
            truthStr = truthTable[curAssnNum][curItemIndex];
            truthTableBox.value += strSoFar + truthStr + "\t|" + "\n";
            
            //itemValsArray[curItemIndex] = truthVal;
            
            //store the current row in the truth table
            for(var i=0; i<curItemIndex; i++)
            {
                //alert("adding from itemValsArray, i=" + i);
                truthTable[curAssnNum][i] = itemValsArray[i];
                
                /*
                //alert("in loop:");
                //alert("curAssnNum: " + curAssnNum
                    + ", i: " + i
                    + ", itemValsArray[i]: " + itemValsArray[i]);
                alert("truthTable[curAssnNum][i]: " + 
                    truthTable[curAssnNum][i]);
                */
            }
            
            //update for the next assignment
            curAssnNum++;
        }
    }
    else if(curItemIndex < numItems-1)
    {
        for(var j=0; j<numTruthVals; j++)
        {
            var truthVal;
            if(j==0)
            {
                truthVal = false;
            }
            else if(j==1)
            {
                truthVal = true;
            }
            truthTable[curAssnNum][curItemIndex] = truthVal;
            
            //alert("in else if storing: " + curAssnNum + ", " + curItemIndex + ": " + truthVal);

            //add truth value to display for current assignment
            var truthStr;
            truthStr = truthTable[curAssnNum][curItemIndex];
            
            //printTruthTableHelper( curItemIndex+1, 
              //  (strSoFar + truthStr + "\t|"), numItems, curAssnNum);
                
            //add truth value to item vals Array
            itemValsArray[curItemIndex] = truthVal;
                
            //printTruthTableHelper( curItemIndex+1, 
              //  (strSoFar + truthStr + "\t|"), numItems, curAssnNum, itemValsArray);
              
                          printTruthTableHelper( curItemIndex+1, 
                (strSoFar + truthStr + "\t|"), numItems, curAssnNum);
                
        }//end for
    }//end else if
    else //curItemIndex > numItems - 1
    {
        updateErrorBox("error generating truth table, " 
            + "curItemIndex: " + curItemIndex
            + "numItems - 1: " + numItems-1 );
    }
}

//get the truth value of an expression
function expressionValue(numTabs, assnIndex)
{
    //alert("in expressionValue, assnIndex: " + assnIndex);
    
    debugBox.value += createTabs(numTabs) + "<expression>" + "\n";

    var value;
    
    formulaStr = skipLeadingBlanks(formulaStr);
    
    value = termValue(numTabs+1, assnIndex);
    
    formulaStr = skipLeadingBlanks(formulaStr);
    
    var nextWord = getFirstWord(formulaStr);
    
    if(nextWord == impliesSym)
    {
        debugBox.value += createTabs(numTabs+1) + "\"" + nextWord +"\"" + "\n";
        
        //remove the word implies
        formulaStr = chompOffFirstWord(formulaStr);
        
        var expressionVal = expressionValue(numTabs+1, assnIndex);
        
        //value -> expressionVal
        //= (not value) or expressionVal
        //alert("value:" + value + " -> " + 
        //    "expressionVal:" + expressionVal + "=");
        value = (!value || expressionVal);
        //alert(value);
    }
 
    debugBox.value += createTabs(numTabs) + "</expression>" + "\n";
    return value;
}//end expressionValue

/*
 Return the truth value of a term.
*/
function termValue(numTabs, assnIndex)
{
    debugBox.value += createTabs(numTabs) + "<term>" + "\n";
    
    //alert("in termValue");
    
    var value;
    
    formulaStr = skipLeadingBlanks(formulaStr);
    
    value = factorValue(numTabs+1, assnIndex);
    
    //alert("after calling factorVal: " + value);
    
    formulaStr = skipLeadingBlanks(formulaStr);
    
    var nextWord = getFirstWord(formulaStr);
    
    //alert("formulaStr: " + formulaStr);
    //alert("next Word: " + nextWord);
    
    while(nextWord == andSym || nextWord == orSym)
    {
        //remove the and, or
        formulaStr = chompOffFirstWord(formulaStr);
        
        debugBox.value += createTabs(numTabs+1) 
            + "\"" + nextWord + "\"" + "\n";
        
        var nextValue = factorValue(numTabs+1, assnIndex);
        
        if(nextWord == andSym)
        {
            //alert(value + " and " + nextValue + "=");
            value = value && nextValue;
            //alert(value);
        }
        else //or
        {
            //alert(value + " or " + nextValue + "=");
            value = value || nextValue;
            //alert(value);
        }
        
        formulaStr = skipLeadingBlanks(formulaStr);
        
        nextWord = getFirstWord(formulaStr);
    }
    
    debugBox.value += createTabs(numTabs) + "</term>" + "\n";
    
    return value;
    
}//end termValue

/*
 Return the truth value of a factor.
*/
function factorValue(numTabs, assnIndex)
{
    debugBox.value += createTabs(numTabs) + "<factor>" + "\n";
    
    //alert("in factorValue");
    
    var value;
    var isNegated = false;
    
    formulaStr = skipLeadingBlanks(formulaStr);
    
    //check for the word not
    var nextWord = getFirstWord(formulaStr);    
    if(nextWord == notSym)
    {
        debugBox.value += createTabs(numTabs+1) 
            + '"' + notSym + '"' + "\n";
         
        //remove the word not
        formulaStr = chompOffFirstWord(formulaStr);
        
        isNegated = true;
    }
    
    //alert("formulaStr: " + formulaStr);
    
    //in case we removed a not, remove the space after not
    formulaStr = skipLeadingBlanks(formulaStr);
    
    var nextChar = getFirstChar(formulaStr);
    
    //check for a left bracket
    if(nextChar == wordLeftSym)
    {
        //remove the left bracket
        formulaStr = chompOffFirstChar(formulaStr);
        
        value = wordValue(numTabs+1, assnIndex);
    }
    
    //check for a left parenthesis
    else if(nextChar == groupLeftSym)
    {
        debugBox.value += createTabs(numTabs+1) 
            + '"' + groupLeftSym + '"' + "\n";
        
        //remove the left parenthesis
        formulaStr = chompOffFirstChar(formulaStr);
                
        value = expressionValue(numTabs+1, assnIndex);
          
        formulaStr = skipLeadingBlanks(formulaStr);
        
        nextChar = getFirstChar(formulaStr);
        
        //check for right parenthesis
        if(nextChar != groupRightSym)
        {
            updateErrorBox("missing " + groupRightSym + "\n");
        }
        else //remove right parenthesis
        {
            debugBox.value += createTabs(numTabs+1) 
                + '"' + groupRightSym + '"' + "\n";
            
            formulaStr = chompOffFirstChar(formulaStr);
        }
    }//end else if
    
    else
    {
        updateErrorBox("unexpected character: " + nextChar + "\n");
    }
    
    if(isNegated)
    {
        value = !value;
    }
    
    debugBox.value += createTabs(numTabs) + "</factor>" + "\n";
    
    return value;
    
}//end factorValue


/*
 Return the truth value of a word.
 Assume that [ has just been chomped off.
*/
function wordValue(numTabs, assnIndex)
{
    debugBox.value += createTabs(numTabs) + "<word>" + "\n";

    //alert("in word value");
    
    var word = "";
    
    var nextChar = getFirstChar(formulaStr);
    
    while(nextChar != wordRightSym && formulaStr.length > 0)
    {
        word += nextChar;
        formulaStr = chompOffFirstChar(formulaStr);
        nextChar = getFirstChar(formulaStr);
    }
    
    if(nextChar != wordRightSym)
    {
        updateErrorBox("missing " + wordRightSym);
    }
    else
    {
        //remove the right bracket
        formulaStr = chompOffFirstChar(formulaStr);
    }
    
    if( !formulaTable.hasItem(word) )
    {
        //formulaTable.setItem(word, startingTruthValue);
        formulaTable.setItem(word, numWordsInTable);
        numWordsInTable++;
        
        //tableBox.value += word + " | " + startingTruthValue + "\n";
        //what if truth value changes?
        tableBox.value += word + " | " + formulaTable.getItem(word) + "\n";
    }
    
    //get the truth value of the word using the given assignment
    //var value = getTruthValue(word, formulaTable);
    var value;
    if(assnIndex == truthTableNotInitVal) //truth table has not been generated yet
    {
        value = startingTruthValue;
    }
    else
    {
        value = truthTable[assnIndex][formulaTable.getItem(word)]; //check this out 
    }
    
    //alert("in wordval:" + "\tword: " + word + "\tvalue: " + value + "\tassnIndex: " + assnIndex);
    
    debugBox.value += createTabs(numTabs+1) + '"' + wordLeftSym + '"' + "\n";
    
    debugBox.value += createTabs(numTabs+1) + word + ": " + value + "\n";
    
    debugBox.value += createTabs(numTabs+1) + '"' + wordRightSym + '"' + "\n";
          
    //tableBox.value += word + " | " + value + "\n";
    
    debugBox.value += createTabs(numTabs) + "</word>" + "\n";
    
    return value;
}//end wordValue

/*
 Update the error box with the latest error.
*/
function updateErrorBox(errorStr) 
{
    errorBox.value += (errorStr + "\n");
}


/*
 Main method of parser - parse and evaluate the expression given in args.
*/
// public static void main(string[] args) {
/*
function main(args)
{
    expressionString = args;
    
    skipBlanks();
    
    //call the expression parser on the expression
    var val = expressionValue(0);
    
    outputBox.value = val;
}
*/


/*
 Return a string with a number of tabs for formatting.
*/
function createTabs(numTabs)
{
    var tabString = "";
    for(var i=0; i<numTabs; i++)
    {
        tabString += "|  ";
    }
    return tabString;
}


/*
 Return the value from parsing an expression.
*/
// private static double expressionValue() throws ParseError {
/*
function expressionValue(numTabs)
{
    debugBox.value += createTabs(numTabs) + "<expression>" + "\n";

    skipBlanks();

    //an expression is made of terms, call the term parser on the next term
    var val = termValue(numTabs+1);
    
    skipBlanks();
    
    //keep reading next term and adding or subtracting it from previous terms
    while(peek() == "+" || peek() == "-")
    {
        var op = getAnyChar();
        debugBox.value += createTabs(numTabs+1) + op + "\n";
         
        var nextVal = termValue(numTabs+1);
        
        if(op == "+")
        {
            val = parseInt(val) + parseInt(nextVal);
        }
        else
        {
            val -= nextVal;
        }
        
        skipBlanks();
    }//end while
    
    debugBox.value += createTabs(numTabs) + "</expression>" + "\n";
    return val;
}//end expressionValue()
*/

/*
 Return the value from parsing a term.
*/
/*
function termValue(numTabs)
{
    debugBox.value += createTabs(numTabs) + "<term>" + "\n";
    
    skipBlanks();
    
    //a term is made of factors, call the factor parser on the next factor
    var val = factorValue(numTabs+1);
    
    skipBlanks();
    
    //keep reading next factor and multiply or dividing previous factors with it
    while(peek() == "*" || peek() == "/")
    {
        var op = getAnyChar();
        debugBox.value += createTabs(numTabs+1) + op + "\n";
        
        var nextVal = factorValue(numTabs+1);
        
        if(op == "*")
        {
            val *= nextVal;
        }
        else
        {
            val /= nextVal;
        }
        
        skipBlanks();       
    }//end while

    debugBox.value += createTabs(numTabs) + "</term>" + "\n";
    return val;
}// end termValue()
*/


/*
 Return the value from parsing a factor.
*/
/*
function factorValue(numTabs)
{
    debugBox.value += createTabs(numTabs) + "<factor>" + "\n";

    skipBlanks();
    
    //var nextChar;
    var nextWord;
    
    var isNegative = false;
    
    if(expressionString.length > 0 )
    {
        //nextChar = expressionString.charAt(0);
        nextWord = peekWord();
     
        //check if factor is negative and chomp off the negative sign
        //check if factor is negated and chomp off not sym
        //if(nextChar == '-')
        if(nextWord == notSym) //TODO: add while loop for multiple not's...
        {
            isNegative = true;
            // expressionString = expressionString.substring(1,expressionString.length);
            
            expressionString = expressionString.substring(notSym.length,expressionString.length);
            skipBlanks(); //remove the space after not sym
            //alert("after chomping not:" + expressionString);
        }
    }
    else
    {
        //alert("expression string length not > 0");
        debugBox.value += createTabs(numTabs+1) + "</factor>" + "\n";
        return -1;
    }
    
    //if a negative was found, we need to advance to the next character
    //if a not sym was found, we need to advance to the next word
    if(isNegative)
    {
    	//nextChar = expressionString.charAt(0);
        nextWord = peekWord();
        //alert("nextWord:" + nextWord);
    }
   	
    //a factor can be a number
    if(isDigit(nextChar) )
    {
        //get the value of the number 
        var factor = getNumber();
        
        //print out parse tree and return value of factor
        if(isNegative)
        {
            debugBox.value += createTabs(numTabs+1) + "<negative>" +  "\n";
            debugBox.value += createTabs(numTabs+2) + factor + "\n";
            debugBox.value += createTabs(numTabs+1) + "</negative>" + "\n";
            debugBox.value += createTabs(numTabs) + "</factor>" + "\n";
            return -factor;
        }
        else
        {
            debugBox.value += createTabs(numTabs+1) + factor + "\n";
            debugBox.value += createTabs(numTabs) + "</factor>" + "\n";
            return factor;
        }
        
    }
    
    //otherwise, factor is an expression in parentheses
    //else if ( nextChar == "(" )
    else if ( nextWord.charAt(0) == groupLeftSym )
    {
        //print out parse tree depending on negativity
        if(isNegative)
        {
            debugBox.value += createTabs(numTabs+1) + "<negative>" +  "\n";
            debugBox.value += createTabs(numTabs+2) + "< ( >" + "\n";
        }
        else
        {
            debugBox.value += createTabs(numTabs+1) + "< ( >" + "\n";
        }
        
        
        //chomp off the "("
        getAnyChar();
        
        var val;
        
        //get the value of the expression
        if(isNegative)
        {
            val = expressionValue(numTabs+3); //add extra tab b/c inside of parenthesis
            val = -val;
        }
        else
        {
            val = expressionValue(numTabs+2); //add extra tab b/c inside of parenthesis
        }
        
        skipBlanks();

        nextChar = expressionString.charAt(0);
        
        //check for the matching right parenthesis
        if(nextChar != ")")
        {
            alert("Missing right  parenthesis aka. ) ");
        }
        else //right parenthesis found
        {
            //print parse tree
            if(isNegative)
            {
                debugBox.value += createTabs(numTabs+2) + "</ ) >" + "\n";
                debugBox.value += createTabs(numTabs+1) + "</negative>" + "\n";
            }
            else
            {
                debugBox.value += createTabs(numTabs+1) + "</ ) >" + "\n";
            }
        
        }
        
        //chomp off the ")"
        getAnyChar();
        
        debugBox.value += createTabs(numTabs) + "</factor>" + "\n";
        
        //return the value of the expression inside of the parentheses
        return val;
    }//end else if left paren
      
    //error checking:
    else if( nextChar == "\n")
    {
        alert("End-of-line encountered in the middle of an expression.");
    }
    else if(nextChar == ")")
    {
         alert("Extra right parenthesis.");         
    }
    else if ( nextChar == '+' || nextChar == '-' || nextChar == '*' || nextChar == '/' )
    {
        alert("Misplaced operator.");
    }
    else
    {
        alert("Unexpected character \"" + nextChar + "\" encountered.");
    }
}//end factorValue()
*/

/*
 Return and chomp off the next number from the expression string.
*/
function getNumber()
{
    //find the first index that is not part of the number
    var i = 0;
    while( isDigit(expressionString.charAt(i))   && i < expressionString.length)
    {
        i++;
    }

    //get value of the number
    var val = expressionString.substring(0,i);

    //chomp off number from expression string
    expressionString = expressionString.substring(i,expressionString.length);
    
    return val;
}//end getNumber()


/*
 Return true if a character is a digit.
*/
function isDigit(charIn)
{
    var validChars = "0123456789";

    for(var i = 0; i<validChars.length;i++)
    {
        if(charIn == validChars.charAt(i) )
        {
        return true;
        }
    }

    return false;
}


/*
 Returns true if the next word is valid, i.e.
 between "[" and "]"
*/
function isWord(word)
{
    //assumes first char is non-blank
    
    //empty word
    if(word.length <= 0)
    {
        return false;
    }
    
    //check for [ and ]
    if(word.charAt(0) == wordLeftSym)
    {
        if(word.charAt(word.length-1) == wordRightSym)
        {
            return true;
        }
        else
        {
            alert("Missing " + wordRightSym);
            return false;
        }
    }
    else
    {
        //don't print error message here
        //because we might be looking at 
        //a keyword or paren
        return false;
    }
}

/*
 Test method - delete this
*/
function test()
{
    // var s1 = "abc";
    // var s2 = "Abc";
    
    // alert( (s1 + "==" + s2 + ": ") + (s1 == s2));
    
    //expressionString = input;
    //peekWord();
    
    
}
